$\forall$$T$:Type, $L$, ${\it L'}$:($T$ List).
\\[0ex]($\neg$($\uparrow$null($L$)))
\\[0ex]$\Rightarrow$ no\_repeats($T$;$L$)
\\[0ex]$\Rightarrow$ ($\neg$($\uparrow$null(${\it L'}$)))
\\[0ex]$\Rightarrow$ ${\it L'}$ $\subseteq$ $L$
\\[0ex]$\Rightarrow$ (last($L$) $\in$ ${\it L'}$)
\\[0ex]$\Rightarrow$ (last(${\it L'}$) = last($L$) $\in$ $T$)